With the ubiquitous presence of software programs permeating almost all aspects of daily life, validating and verifying software in order to provide robust and reliable software programs has become a necessity. Traditionally, software quality has been assured through manual testing, which may be tedious, difficult, and often gives poor coverage of the source code. More recently, techniques for formally validating software programs have been developed. One such technique is symbolic execution.
Symbolic execution is a non-explicit state model-checking technique that treats input to a software program as symbol variables. It creates complex equations by executing all finite paths in the software program with symbolic variables and then solves the complex equations with a solver, typically known as a decision procedure, to obtain error scenarios, if any. In contrast to explicit state model checking, symbolic execution is able to work out all possible input values and all possible use cases of all possible input values in the software program under analysis. Symbolic execution can be used to automatically generate test inputs with high structural coverage for the program under analysis.